\documentclass{llncs}
\usepackage{url}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}
\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}
\newcommand{\text}[1]{\mbox{#1}}
\newcommand{\wc}{\_}
\newcommand{\mulstep}{ \stackrel{*}{\leadsto}}
\newcommand{\lam}[2]{\lambda #1 . #2}
\newcommand{\evals}[2]{#1 \downarrow #2}
\newcommand{\wm}[0]{\stackrel{\textit{w}}{\to}}
\newcommand{\interp}[1]{[\negthinspace[#1]\negthinspace]}
\newcommand{\symm}[1]{\langle\textit{#1}\rangle}
\newcommand{\rrl}[1]{\textit{r-#1}}
\newcommand{\rrlb}[0]{\textit{r-}\beta}
\newcommand{\trl}[1]{\textit{t-#1}}
\begin{document}
%\pagestyle{empty}
\title{Learning Category Theory}
\author{Peng Fu}
\institute{Computer Science, The University of Iowa}
\date{June 29, 2012}


\maketitle
\thispagestyle{empty}

\section{Introduction}

\noindent This file is mainly for me to learn and try to formulate the language of category theory. I use Saunders Mac Lane's \textit{category theory for the working mathematician} as reference.
\section{Basic Concepts}

\subsection{Metacategory}

\begin{definition}[Metacategory]
%% \noindent A \textit{metacategory} is a tuple $(\mathcal{C}, \mathsf{dom}, \mathsf{cod},\mathsf{id}, \circ)$, where $\mathsf{Obj} (\mathcal{C}),\mathsf{Mor}(\mathcal{C})$ are classes, and for $A, B \in \mathsf{Obj} (\mathcal{C}), \mathsf{Hom}(A, B) \in \mathsf{Mor} (\mathcal{C})$. $\mathsf{dom}, \mathsf{cod}: \mathsf{Mor}(\mathcal{C}) \rightarrow \mathsf{Obj}(\mathcal{C})$. $\mathsf{id}: \mathsf{Obj}(\mathcal{C}) \rightarrow \mathsf{Mor}(\mathcal{C})$, $\circ: \mathsf{Mor}(\mathcal{C}) \times \mathsf{Mor}(\mathcal{C}) \rightarrow \mathsf{Mor}(\mathcal{C})$ are functions.
%% They satisfy following axioms

\

\begin{tabular}{lllll}
\infer{\mathsf{Obj} (\mathcal{C}) :  \mathsf{Category}}{}

& & & &

\infer{ \mathsf{Hom}_{\mathcal{C}}(A,B) :  \mathsf{Category}}
{A : \mathsf{Obj} (\mathcal{C}) && B : \mathsf{Obj} (\mathcal{C})}

\\

\\

\infer={ \mathsf{Hom}_{\mathcal{C}}(A,B) = \mathsf{Hom}_{\mathcal{C}}(X,Y) : \mathsf{Category} }
{A = X: \mathsf{Obj} (\mathcal{C}) & B = Y: \mathsf{Obj} (\mathcal{C})}

&  & & & 

\infer{ \mathsf{id} A : \mathsf{Hom}_{\mathcal{C}}(A,A)}
{}

\\

\\


\infer{ g\circ f :  \mathsf{Hom}_{\mathcal{C}}(A,C) }
{ f:  \mathsf{Hom}_{\mathcal{C}}(A,B) &&  g : \mathsf{Hom}_{\mathcal{C}}(B,C)}

& & & &

\infer{ f \circ (\mathsf{id} A) =  f :  \mathsf{Hom}_{\mathcal{C}}(A,B) }
{ f:  \mathsf{Hom}_{\mathcal{C}}(A,B)}

\\

\\

\infer{ (\mathsf{id} B) \circ f  =  f :  \mathsf{Hom}_{\mathcal{C}}(A,B) }
{ f:  \mathsf{Hom}_{\mathcal{C}}(A,B)}

& & & &

\infer{ (h\circ g)\circ f = h\circ (g\circ f) :  \mathsf{Hom}_{\mathcal{C}}(A,D) }
{ f:  \mathsf{Hom}_{\mathcal{C}}(A,B) &&  g : \mathsf{Hom}_{\mathcal{C}}(B,C) & h : \mathsf{Hom}_{\mathcal{C}}(C,D)}


\\
\end{tabular}
\end{definition}


\begin{definition}[Equality]

\

\noindent Reflexivity

\

\begin{tabular}{lll}

\infer{A = A}{A :  \mathsf{Category}}

& &

\infer{a = a}{a :  A}

\end{tabular}

\

\noindent Symmetry 

\

\begin{tabular}{lll}

\infer{b = a}{a = b :  A}

& &

\infer{B = A}{A = B :  \mathsf{Category}}

\end{tabular}

\

\noindent Transitivity

\

\begin{tabular}{lll}

\infer{a = c:A}{a = b :  A & b = c :  A}

& &

\infer{A = C}{A = B :\mathsf{Category}  & B = C :  \mathsf{Category}}

\end{tabular}



\end{definition}

\noindent \textbf{Remarks}: Here $\mathsf{Category}$ is in the sense of Per Martin-l$\ddot{o}$f's \textit{intuitionistic type theory}, namely,`` a category is defined by explaining what an object of the category is and when two such objects are equal''.

\subsection{Functor and Natural Transformation}

\begin{definition}[(covariant)Functor]

\

\begin{tabular}{lllll}

\infer{\mathcal{A} \rightarrow \mathcal{B} :  \mathsf{Category}}{}

& & & &

\infer{T c  :  \mathsf{Obj}(\mathcal{B}) }{T: \mathcal{A} \rightarrow \mathcal{B} & c : \mathsf{Obj}(\mathcal{A}) }


\\

\\

\infer{ T f  :  \mathsf{Hom}_{\mathcal{B}}(T A, T B) }{T: \mathcal{A} \rightarrow \mathcal{B} & f : \mathsf{Hom}_{\mathcal{A}}(A,B)}

& & & &


\infer{ T(\mathsf{id} A) = \mathsf{id} (T A):\mathsf{Hom}_{\mathcal{B}}(T A, T A) }
{T: \mathcal{A} \rightarrow \mathcal{B} &  A : \mathsf{Obj}(\mathcal{A}) }


\\

\\

\infer{ T(g \circ f) =  Tg \circ Tf: \mathsf{Hom}_{\mathcal{B}}(T A, T C) }
{T: \mathcal{A} \rightarrow \mathcal{B} & g : \mathsf{Hom}_{\mathcal{A}} (B,C) & f : \mathsf{Hom}_{\mathcal{A}} (A,B)}


\\
\end{tabular}


\end{definition}

\begin{definition}[Contravariant Functor]

\

\begin{tabular}{lllll}

\infer{\mathcal{A} \rightarrow \mathcal{B} :  \mathsf{Category}}{}

& & & &

\infer{T c  :  \mathsf{Obj}(\mathcal{B}) }{T: \mathcal{A} \rightarrow \mathcal{B} & c : \mathsf{Obj}(\mathcal{A}) }


\\

\\

\infer{ T f  :  \mathsf{Hom}_{\mathcal{B}}(T B,T A) }{T: \mathcal{A} \rightarrow \mathcal{B} & f : \mathsf{Hom}_{\mathcal{A}}(A,B)}

& & & &


\infer{ T(\mathsf{id} A) = \mathsf{id} (T A):\mathsf{Hom}_{\mathcal{B}}(T A, T A) }
{T: \mathcal{A} \rightarrow \mathcal{B} &  A : \mathsf{Obj}(\mathcal{A}) }


\\

\\

\infer{ T(g \circ f) = Tf \circ Tg : \mathsf{Hom}_{\mathcal{B}}(T C, T A) }
{T: \mathcal{A} \rightarrow \mathcal{B} & g : \mathsf{Hom}_{\mathcal{A}} (B,C) & f : \mathsf{Hom}_{\mathcal{A}} (A,B)}


\\
\end{tabular}


\end{definition}

\begin{definition}[Natural Transformation]

\

\begin{tabular}{lllll}

\infer{ S \rightarrow T :  \mathsf{Category}}{S, T :\mathcal{A} \rightarrow \mathcal{B}}

& & & &

\infer{\tau c  :  \mathsf{Hom}_{\mathcal{B}}(S c, T c) }{\tau: S \rightarrow T & S, T :\mathcal{A} \rightarrow \mathcal{B} & c: \mathsf{Obj}(\mathcal{A}) }


\\

\\

\infer{\tau A \circ T f = S f \circ \tau B  :  \mathsf{Hom}_{\mathcal{B}}(S A, T B) }{\tau: S \rightarrow T & S, T :\mathcal{A} \rightarrow \mathcal{B} & f: \mathsf{Hom}_{\mathcal{A}}(A,B)}


\\
\end{tabular}


\end{definition}

\section{Constructions on Categories}

\subsection{Contravariance and Opposites}
\begin{definition}[Opposite category]

\

\begin{tabular}{lllll}
\infer{\mathsf{Obj} (\mathcal{C}^{op}) :  \mathsf{Category}}{\mathsf{Obj} (\mathcal{C}) :  \mathsf{Category}}

& & & &

\infer={c:\mathsf{Obj} (\mathcal{C}^{op})}{c:\mathsf{Obj} (\mathcal{C})}


\\

\\


\infer={ f^{op} :  \mathsf{Hom}_{\mathcal{C}^{op}}(B,A) }
{ f:  \mathsf{Hom}_{\mathcal{C}}(A,B) }

& & & &


\infer{(g \circ f)^{op} = f^{op} \circ g^{op}:  \mathsf{Hom}_{\mathcal{C}^{op}}(C,A) }
{ f:  \mathsf{Hom}_{\mathcal{C}}(A,B) && g:  \mathsf{Hom}_{\mathcal{C}}(B,C) }

\\
\end{tabular}
\end{definition}

\noindent We can define contravariance functor with the help of opposite category, let $F: \mathcal{A} \rightarrow \mathcal{B}$ be a covariant functor, the contravariance functor will be the covariant functor $G: \mathcal{A}^{op} \rightarrow \mathcal{B}$. \textit{opposite functor} $F^{op} :\mathcal{A}^{op} \rightarrow \mathcal{B}^{op} $. We also have $(F^{op})^{op} = F$.

\subsection{Products of Categories}
\begin{definition}[Product]

\

\begin{tabular}{lllll}
\infer{\mathsf{Obj} (\mathcal{B}\times \mathcal{C}) :  \mathsf{Category}}{\mathsf{Obj} (\mathcal{B}),\mathsf{Obj} (\mathcal{C}) :  \mathsf{Category}}

& & & &

\infer{(b,c) :\mathsf{Obj} (\mathcal{B}\times \mathcal{C}) }{b:\mathsf{Obj}(\mathcal{B})&& c: \mathsf{Obj} (\mathcal{C})}


\\

\\


\infer{ (f,g) :  \mathsf{Hom}_{\mathcal{B}\times \mathcal{C}}((A,C),(B,D)) }
{ f:  \mathsf{Hom}_{\mathcal{B}}(A,B) && g:  \mathsf{Hom}_{\mathcal{C}}(C,D) }

& & & &

\infer{ (f',g')\circ(f,g) = (f'\circ f,g'\circ g)  :  \mathsf{Hom}_{\mathcal{B}\times \mathcal{C}}((A,C),(E,F)) }
{ (f,g) :  \mathsf{Hom}_{\mathcal{B}\times \mathcal{C}}((A,C),(B,D)) && (f',g') :  \mathsf{Hom}_{\mathcal{B}\times \mathcal{C}}((B,D),(E,F)) }


\\
\end{tabular}
\end{definition}

\begin{definition}[Projection Functor]

\

\begin{tabular}{lllll}

\infer{\mathcal{B}\times \mathcal{C} \rightarrow \mathcal{B} :  \mathsf{Category}}{}

& & & &

\infer{\mathcal{B}\times \mathcal{C} \rightarrow \mathcal{C} :  \mathsf{Category}}{}


\\

\\

\infer{P (b,c) = b  :  \mathsf{Obj}(\mathcal{B}) }{P: \mathcal{B}\times \mathcal{C} \rightarrow \mathcal{B} & (b,c) : \mathsf{Obj}(\mathcal{B}\times \mathcal{C}) }



& & & &

\infer{Q (b,c) = c :  \mathsf{Obj}(\mathcal{B}) }{Q: \mathcal{B}\times \mathcal{C} \rightarrow \mathcal{C} & (b,c) : \mathsf{Obj}(\mathcal{B}\times \mathcal{C}) }


\\

\\

\infer{ T(g \circ f) = Tf \circ Tg : \mathsf{Hom}_{\mathcal{B}}(T C, T A) }
{T: \mathcal{A} \rightarrow \mathcal{B} & g : \mathsf{Hom}_{\mathcal{A}} (B,C) & f : \mathsf{Hom}_{\mathcal{A}} (A,B)}


\\
\end{tabular}


\end{definition}



\end{document}
